00050 VAR: X,Y,Z,U,V; 00075 PRE_PRED: A,B; 00087 PRE_OP: 0,1,2,3; 00093 INDUCT: 00100 (A(0)∨B(0))∧(A(1)∨B(1)⊃(A(2)∨B(2))) ⊃(A(3)∨B(3)); 00300 BASIS: A(0)∨B(0); 00400 STEP: A(1)∨B(1)⊃(A(2)∨B(2)); 00600 THEOREM: A(3)∨B(3); 00700 ;